00050	
00100	INF_OP: * ,⊗;
00200	INF_PRED: =;
00300	EQUALITY: =;
00400	VAR: x ,y,s,t,r,z,u,v,w;
00500	PRE_OP: N,rev,list,car,cdr; 
00600	PRE_PRED: null;
00700	A1A: rev(N)=N;
00800	A1B: ¬null(y)⊃(rev(y)=rev(cdr(y))*list(car(y)));
00900	A2A: N*u =u;
01000	A2B:u*N=u;
01100	A3: u*(v*w)=(u*v)*w;
01200	A4: list(u)*v =u⊗v;
01300	
01400	lemmaA: ∃y∃z rev(y)*z=rev(x);
01500	THEOREM: ∀(s,t)∃r(¬null(s) ∧(rev(s)*t =rev(x)) ⊃ (rev(cdr(s))*r =rev(x)));
01600	;